COMMENT ⊗   VALID 00010 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	1987 sept 12
C00004 00003	1987 sept 26
C00006 00004	1987 sept 28
C00008 00005	1987 Oct 4
C00009 00006	****
C00015 00007	Elephant logic
C00026 00008	Notes on knowledge
C00027 00009	Mental situations
C00035 00010	Elephant logic
C00045 ENDMK
C⊗;
1987 sept 12

I need to make progress in turning conceptual problems into technical
problems.  It seems likely that I can do this with the problem of
giving priority to the normality of what is known over the normality
of that which is derived from it.  The example of beating the defaults
of American women by facts derived from the fact that the woman is a
particular person's mother looks good.

¬ab aspect1 x ⊃ nationality mother x = nationality x

nationality Sam = British

¬ab aspect2 z ⊃ nationality z = American

This gives a conflict, so we need to reify enough to express the priority
that what we know about someone's mother as derived from what we know
about him takes precedence over defaults on the person.

Maybe we need some more reified entities --- for example, "all I know about X".

1987 sept 26

Declarative expression of reasoning heuristics

1. Use elephant in the expression of the heuristics, i.e. allow
reference to past beliefs and inferences.  In particular, we can
allow rules of the form "do X if it hasn't already been done".

2. good-to-apply(rule, data, s)

3. goal(show(congruent(tri1,tri2)),s) ∧
have(equal(side(AB,tri1),side(AB,tri2)),s) ∧
have(equal(side(AC,tri1),side(AC,tri2)),s) ⊃
goal1(show(equal(angle(A,tri1),angle(A,tri2)),s)

This is true, but we need some way of saying that this
should be tried before trying to prove some other
instantiation of side-angle-side for which we don't
have two of the premisses already.

derived(mother Nilsson, Nilsson, s)
1987 sept 28

emphasize that the boat can be presumed to be usable because
it is there for a purpose.

Can we have the clarity of the Peirera-Porto coloring program
without its presumptive algorithm?

In order to prove that something cannot happen, we need to
enumerate possible events and prove that each of them
preserves a predicate incompatible with what we want to
prove cannot happen.  However, there is a simpler case of
prevention.  When A grabs B to prevent him from walking in
front of a car, he isn't saving B forever from being run
over, he is just preventing a particular event.  Include
prevention in the situation calculus discussion in class,
especially contrasting it with STRIPS, Prolog and other purely
computational formalisms.

Distinguish purely computational formalisms.
1987 Oct 4

It seems we cannot avoid designating some terms as primitive in
order to make frames.  However, we can make the designations
of what is primitive context-dependent.
****

The following is related to the non-monotonic reasoning required
for the Yale shooting problem but by a chain of steps that may
be tenuous.  Our current approach involves reifying reasons and
saying that nothing occurs without a reason.  Shooting is a reason
for dying, though not a conclusive one, but there is no reason for
the gun to become unloaded.  (This is especially true if the
Yale shooting scenario is a story or a plan).  I worried that
our intuitive view of this may bog down when we try to formalize
it, because this intuitive view is founded on looking at the
database from the outside, i.e. have sentences that aren't in
the database but meta to it.

Trying to invent suitable predicates and functions of databases
has been frustrating, and the following is a conjecture of why
and what might be done about it.

Suppose the basic object isn't just the database but the database
+ metalinguistic commentary.  The predicates on databases refer
to the commentary as well as to the database itself.

Note: {p,p∧q} has the same extension as {p∧q} but isn't the same
database, because there may be operations that work on the
separated  p.  {p,q} is clearer, because it suggests that  p  and
q  can be modified separately.

One kind of commentary is derivation information, e.g. that  q
came from  p  and  p ⊃ q by modus ponens.

****

Let's think about an Elephant Prolog that only adds to its database,
and everything in it remains true.  However, some of the information
initially and also deduced is meta-information.  All of Prolog's
hidden information, e.g. goal and proof trees, are to be explicit
meta-information.

Such a system might record stages, e.g. by successively proving
is-stage(0), is-stage(1), etc.  Meta-sentences may have stage
arguments and can thus assert what isn't known at a given stage.
Everything deduced is eternally true.  The deduction routines
pay attention to what stage has been reached.  They may have
negative premisses about what has been deduced, and this somehow
suggests that we try to make them get by with negation as failure.

Maybe Apt will be interested in this.

Oct 8

Elephant logic

The axioms are such that all results of inference include their history.
The simplest kind of axiom that works for this is

b(p,r1) ∧ b(p imp q,r2) ⊃ b(q,mp(p,q,r1,r2)).

However, this doesn't contain enough information about the state
of the database to do non-monotonic reasoning.  For this we need
the database as a parameter and axioms that describe how it changes.

holds(p,r1,db) ∧ holds(p imp q,r2,db) ⊃
holds(q,mp(p,q,r1,r2),result(mp(p,q,r1,r2),db))

We also require

holds(p,r,db) ⊃ holds(p,r,result(mp(x,y,z,w),db))

or the two sentences

holds(p,r,db) ∧ monotonic e ⊃ holds(p,r,result(e,db))

∀x y z w.monotonic mp(x,y,z,w)

which express the monotonicity of modus ponens.

In order to get an example of non-monotonicity, it seems easiest to
take an example from default logic.

rule(name(p,Mq,r),db) ∧ holds(p,r1,db) ∧ consistent(q,db) ⊃
	holds(r,default(name,p,q,r),r1),result(default(name(p,q,r),r1),db)).

See elephant-logic.text for more.

Oct 8

What are the functional requirements for communication?  This is
the question the linguists fail to treat.  These requirements
involve the knowledge of the sender and recipient including linguistic
knowledge.

Oct 9

isrel(s)

is a predicate on situation, to be minimized in some way, that
tells what situations we are interested in.  We might have

isrel s0 ∧ isrel result(load,s0) ∧ isrel(load*wait,s0) ∧ 
	isrel(load*wait*shoot,s0)

and circumscribe  ab  only over the relevant situations.
Elephant logic

The axioms are such that all results of inference include their history.
The simplest kind of axiom that works for this is

b(p,r1) ∧ b(p imp q,r2) ⊃ b(q,mp(p,q,r1,r2)).

However, this doesn't contain enough information about the state
of the database to do non-monotonic reasoning.  For this we need
the database as a parameter and axioms that describe how it changes.

holds(p,r1,db) ∧ holds(p imp q,r2,db) ⊃ holds(q,mp(p,q,r1,r2),result(mp(p,q,r1,r2),db))

We also require

holds(p,r,db) ⊃ holds(p,r,result(mp(x,y,z,w),db))

or the two sentences

holds(p,r,db) ∧ monotonic e ⊃ holds(p,r,result(e,db))

∀x y z w.monotonic mp(x,y,z,w)

which express the monotonicity of modus ponens.

In order to get an example of non-monotonicity, it seems easiest to
take an example from default logic.

rule(name(p,Mq,r),db) ∧ holds(p,r1,db) ∧ consistent(q,db) ⊃
	holds(r,default(name,p,q,r),r1),result(default(name(p,q,r),r1),db))

Of course, this gives no opportunity to infer new rules.  I suppose this
still preserves all information in the database, but it mightn't preserve
something like

follows(p,db)

if non-monotonic rules were involved in the derivation of  p,
which the preceding axiom would.  Thus we have

follows(q,db) ⊃ follows(q,result(mp(x,y,z,w),db)).

or

follows(q,db) ∧ monotonic e ⊃ follows(q,result(e,db)).

The next tasks seem to be:

1. Formalize all prop-calc in one go, i.e. with predicate prop-calc.

2. Look at reasoning involving variables.

3. Do a heuristic.

4. Do the predicates that permit expressing a preference for
the acceptance of results early in the reasoning.  This is the
main goal of elephant-logic.

Maybe we need a name that doesn't confuse people into thinking
it's a new form of logic.  Perhaps an elephant metatheory of
first order logic.  Maybe the Elephant logical language.

We need to be able to say, "What we know about Y is derived from
what we know about X".  We also need  abnormality(X).  Then we can
say

derived(Y,X) ⊃ prefer(abnormality(Y),abnormality(X)).

****
October 9 (Timothy is 23 months)

Perhaps we don't need to derive the history explicitly in the axioms.
Instead we can refer to the history as a function of the wff and the
database.
Actually let's consider  P  to be an occurrence of a formula  p  rather than
the abstract formula itself.  It's the occcurrences that have histories
rather than the formulas themselves.

We have

wff(P)

and

occurrences(p,s)

which may be  nil.


We have the predicate

observation(P,s)

which is true if  P  entered the database  s  by observation.

We also have

from-mp(P,s)

if  P  entered  s  by a modus ponens.

In that case the functions  major(P,s)  and  minor(P,s)  are defined
as the occurrences of the major and minor premisses of  P.

We now have

result(modus(P1,P2),s)

which is the database that results from performing a modus ponens with
premisses  P1  and  P2.  Very likely we want to require that when
P1 and P2 do not admit a modus ponens, then

result(modus(P1,P2),s) = s.

Perhaps it is useful to allow formulas like EKL proof checker commands.
For example, we can have

result(derive(p,U),s).

This is the database that results from attempting to derive the wff p
from the set U of occurrences of wffs in the database s.  If the
derivation of p from U is successful, then result(derive(p,U),s) is s
extended by a new occurrence of p.  On the other hand, if the action
derive(p,U)  is unsuccessful, then result(derive(p,U),s)
is  s  extended by an occurrence of

not derivable(p,U,s).

We will need names for sets of occurrences that include at least
explicit listing and also the whole database.  We may also need
variants with different concepts of derivation.

This statement can be used as a premiss in non-monotonic rules.  However,
there is a small complication.  The system may have reached the conclusion that
something was not derivable several steps previous to the time it wants to
be used.  It's still ok to use it, provided all the reasoning in between
was monotonic, i.e. what was proved several steps previously still holds
and is an adequate premiss.  This means that the rules of inference must
allow reference to such previously shown database referential statements.
But this is just the kind of elephantine property that should be expected.

	Rewrite commands as in EKL should also be useful.

	Do we need the formula

latest(s)

for the latest formula in a database?  If we have it, we can write

P1 ε s ∧ P2 ε s ∧ ok-mp(wff(P1),wff(P2)) ⊃ from-mp(latest(result(modus(P1,P2),s)))

and similar axioms.

Sentences about the database itself. WE UPSTAGED THIS POINT.

To avoid paradox we should not have sentences about  s  within  s,
but there is nothing to prevent there being sentences about the
predecessors of  s.  If we assume that formulas are added to  s
successively, then the function

pred(s)

is defined and gives the preceding database.

We can have queries about a database, but these give rise to
new databases.  Consider for example

result(query p,s).

We will have either

occurs(in(p,s),result(query p,s))

or

occurs(not in(p,s),result(query p,s)).

More complex queries can be made, e.g. whether a certain wff
is a consequence of the database.  The result of such a query
can be entered in the next database or it can merely serve
as the premiss of some deduction.

Question: Do the logical operations combine wffs or occurrences
of wffs?  Do we have  p and q  or  P and Q?  The latter is
more powerful in terms of the ability to express heuristics,
but may not be necessary.

Maybe the next problem is to see what we need to express a heuristic.

Goals

	We want to treat goals and generated subgoals.  Is there
anything wrong with having

occurs(goal p,s)

in the database?

	Consider the action  assume(p)  leading to the database

result(assume p,s).

	We allow it, but the pedigree of the resulting occurrence
of  p  includes the fact that it is an assumption.  It suggests
also having the function

assumptions(P,s)

giving the assumptions used in deriving the wff-occurrence  P.
We will abbreviate "wff-occurrence" by "wffo".  We clearly
need an analog of the natural deduction rule ⊃i that discharges
assumptions.

1987 Oct 30

Maybe we don't need so many mental situations.  We surely need
a new one whenever we observe the present situation and reach
a non-monotonic conclusion about it.
Notes on knowledge

Let's formalize knowledge using circumscription.

Key axiom:

cancels(x,y) ∧ applies(x,s) ⊃ ab aspect1(y,s).

This is intended to allow cancellation of inheritance, but
it isn't quite right.

We want a general axiom that says that people know the effects
of their possible actions.  It should be cancellable by consideration
that says they don't, e.g. a person doesn't ordinarily know the
combination of a safe, but he ordinarily does if it's his safe.

relevant(x,p,s) ∧ ¬ab aspect1(p,x,s) ⊃ holds(knows(p,x),s)

cancels(issafe y,knows(p,combination y))

Mental situations

	(McCarthy 1960) proposes an Advice Taker program that would represent what it
knew by logical sentences and decide what to do by logical inference.
That paper further promised that even the heuristics that guide the reasoning
strategy would be represented by sentences.  While some progress has been
made in representing facts about the effects of actions by logical sentences,
and non-monotonic reasoning has been formalized in various ways and added
to logical deduction as a means of deciding what to do, I don't know of
any progress in expressing reasoning heuristics declaratively.

	The present paper introduces the idea of mental situation as a
generalization of a database and applies it to formalizing heuristics.
Both in AI and in database theory, one normally thinks of a database as
a collection of sentences about some object domain.  If the computer
keeps any information about the inferential history of the sentences, as
RMS's do, this information is represented other than by sentences.  The
mental situations we introduce in this paper represent inferential
history also by sentences --- at least sentences about the history of
the database can be used as premisses in inferences.  The present
proposal can be regarded as a generalization of the RMS idea.  However,
the history information is represented declaratively itself and can be
used as premisses in arbitrary sentences used to decide what to do.

	Let there be some base language $L$ with a certain class of wffs.
The basic element of our database isn't a wff but an occurrence of
a wff.  We need occurrences rather than just wffs, because the same
wff may have been derived in different ways.  Here are our conventions.

We will list the variables ranging over various kinds of entities.  A
letter representing a variable with primes or subscripts has the same
range as the letter plain.  The letter $s$ is a situation variable.  $S$
is a situation constant.  The variable $P$ ranges over occurrences and
$p$ over wffs.

$wff(P)$ is the wff of which $P$ is an occurrence.

$occurrences(p,s)$ is the set of occurrences of the wff $p$, and $occurs(p,s)$
is an abbreviation of $occurrences(p,s) ≠ \{\}$.

	Mental events give rise to new situations.  $result(modus(P1,P2),s)$
is the situation that results from applying the modus ponens rule of inference
in the situation $s$.  If the rule is applicable, there is a new occurrence
of the result of the rule in this situation.  If the rule is inapplicable,
there is an occurrence of
%
$$fails(modus(P1,P2),s).$$
%
Thus we see that situations can be mentioned in sentences, although we provide
no way for a situation to refer to itself.

Uses of Mental Situations

	The most direct way to use a program that keeps track of mental situations
is manually, i.e. as a reasoning checker or interactive reasoner.  The user
manually issues commands like $modus(P1,P2)$.  Let's call such a program R1,
for ``reasoner-1''.  R1 needs many more commands, i.e. there need to be many
more mental actions before it can be as good an interactive theorem prover
as, say, Ketonen's (19xx) EKL.  For example, the use of sentences as rewrite
rules needs to be allowed.  Defining collections of sentences as rewrite rules
needs to result in sentences being put in the database.  R1 will be more
powerful than EKL, because it can include sentences that refer to mental
situations, i.e. the ones that arose earlier in the reasoning.  The database
can also include sentences that quantify over mental situations.

	The next step is a program that executes the mental action commands
and uses mental queries to decide what to do.  The key question is the
extent to which the reasoning strategy is imbedded in the program and
the extent to which it is represented in the mental situation itself.  The
goal is a very simple program with all strategy represented in the situation.

from notebook - 1987 Oct 24

active predicates

The rules for deciding what to do contain ``active predicates'' referring
to the current mental situation as well as static facts incorporated in
the mental situation.  The evaluation of an active predicate (active fluent)
results in a sentence about the situation being included in the resulting
situation, but it also as a dynamic effect in causing the rule to be
activated.

	Also the basic thinking mechanism may use stacks, but the state
of these stacks is also represented by sentences --- possibly only
virtual sentences.

***

Notes

1987 Dec 11

	The program that matches the test side of rules accepts as premisses
sentences from old versions of the database that haven't been actively
forgotten.  However, when it achieves a match, it checks whether the premisses
may all be considered current.  This is (normally) a dynamic process, i.e. it
doesn't add sentences to the database. 

Elephant logic

The axioms are such that all results of inference include their history.
The simplest kind of axiom that works for this is

b(p,r1) ∧ b(p imp q,r2) ⊃ b(q,mp(p,q,r1,r2)).

However, this doesn't contain enough information about the state
of the database to do non-monotonic reasoning.  For this we need
the database as a parameter and axioms that describe how it changes.

holds(p,r1,db) ∧ holds(p imp q,r2,db) ⊃ holds(q,mp(p,q,r1,r2),result(mp(p,q,r1,r2),db))

We also require

holds(p,r,db) ⊃ holds(p,r,result(mp(x,y,z,w),db))

which expresses the monotonicity of modus ponens.

In order to get an example of non-monotonicity, it seems easiest to
take an example from default logic.

rule(name(p,Mq,r),db) ∧ holds(p,r1,db) ∧ consistent(q,db) ⊃
	holds(r,default(name,p,q,r),r1),result(default(name(p,q,r),r1),db))

Of course, this gives no opportunity to infer new rules.  I suppose this
still preserves all information in the database, but it mightn't preserve
something like

follows(p,db)

if non-monotonic rules were involved in the derivation of  p,
which the preceding axiom would.  Thus we have

follows(q,db) ⊃ follows(q,result(mp(x,y,z,w),db)).

The next tasks seem to be:

1. Formalize all prop-calc in one go, i.e. with predicate prop-calc.

2. Look at reasoning involving variables.

3. Do a heuristic.

4. Do the predicates that permit expressing a preference for
the acceptance of results early in the reasoning.  This is the
main goal of elephant-logic.

Maybe we need a name that doesn't confuse people into thinking
it's a new form of logic.  Perhaps an elephant metatheory of
first order logic.

We need to be able to say, "What we know about Y is derived from
what we know about X".  We also need  abnormality(X).  Then we can
say

derived(Y,X) ⊃ prefer(abnormality(Y),abnormality(X)).

****
October 9 (Timothy is 23 months)

Perhaps we don't need to derive the history explicitly in the axioms.
Instead we can refer to the history as a function of the wff and the
database.
Actually let's consider  P  to be an occurrence of a formula  p  rather than
the abstract formula itself.  It's the occcurrences that have histories
rather than the formulas themselves.

We have

wff(P)

and

occurrences(p,s)

which may be  nil.


We have the predicate

observation(P,s)

which is true if  P  entered the database  s  by observation.

We also have

from-mp(P,s)

if  P  entered  s  by a modus ponens.

In that case the functions  major(P,s)  and  minor(P,s)  are defined
as the occurrences of the major and minor premisses of  P.

We now have

result(modus(P1,P2),s)

which is the database that results from performing a modus ponens with
premisses  P1  and  P2.  Very likely we want to require that when
P1 and P2 do not admit a modus ponens, then

result(modus(P1,P2),s) = s.

Perhaps it is useful to allow formulas like EKL proof checker commands.
For example, we can have

result(derive(p,U),s).

This is the database that results from attempting to derive the wff p
from the set U of occurrences of wffs in the database s.  If the
derivation of p from U is successful, then result(derive(p,U),s) is s
extended by a new occurrence of p.  On the other hand, if the action
derive(p,U)  is unsuccessful, then result(derive(p,U),s)
is  s  extended by an occurrence of

not derivable(p,U,s).

We will need names for sets of occurrences that include at least
explicit listing and also the whole database.  We may also need
variants with different concepts of derivation.

This statement can be used as a premiss in non-monotonic rules.  However,
there is a small complication.  The system may have reached the conclusion that
something was not derivable several steps previous to the time it wants to
be used.  It's still ok to use it, provided all the reasoning in between
was monotonic, i.e. what was proved several steps previously still holds
and is an adequate premiss.  This means that the rules of inference must
allow reference to such previously shown database referential statements.
But this is just the kind of elephantine property that should be expected.

	Rewrite commands as in EKL should also be useful.

	Do we need the formula

latest(s)

for the latest formula in a database?  If we have it, we can write

P1 ε s ∧ P2 ε s ∧ ok-mp(wff(P1),wff(P2)) ⊃ from-mp(latest(result(modus(P1,P2),s)))

and similar axioms.

Sentences about the database itself. WE UPSTAGED THIS POINT.

To avoid paradox we should not have sentences about  s  within  s,
but there is nothing to prevent there being sentences about the
predecessors of  s.  If we assume that formulas are added to  s
successively, then the function

pred(s)

is defined and gives the preceding database.

We can have queries about a database, but these give rise to
new databases.  Consider for example

result(query p,s).

We will have either

occurs(in(p,s),result(query p,s))

or

occurs(not in(p,s),result(query p,s)).

More complex queries can be made, e.g. whether a certain wff
is a consequence of the database.  The result of such a query
can be entered in the next database or it can merely serve
as the premiss of some deduction.

Question: Do the logical operations combine wffs or occurrences
of wffs?  Do we have  p and q  or  P and Q?  The latter is
more powerful in terms of the ability to express heuristics,
but may not be necessary.

Maybe the next problem is to see what we need to express a heuristic.

Goals

	We want to treat goals and generated subgoals.  Is there
anything wrong with having

occurs(goal p,s)

in the database?

	Consider the action  assume(p)  leading to the database

result(assume p,s).

	We allow it, but the pedigree of the resulting occurrence
of  p  includes the fact that it is an assumption.  It suggests
also having the function

assumptions(P,s)

giving the assumptions used in deriving the wff-occurrence  P.
We will abbreviate "wff-occurrence" by "wffo".  We clearly
need an analog of the natural deduction rule ⊃i that discharges
assumptions.

1987 Oct 30

Maybe we don't need so many mental situations.  We surely need
a new one whenever we observe the present situation and reach
a non-monotonic conclusion about it.